\begin{tabbing} rv{-}identically{-}distributed($p$;$n$.$f$($n$);$i$.$X$($i$)) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$n$:$\mathbb{N}$, $m$:$\mathbb{N}$.\+ \\[0ex]expectation($p$;$f$($n$);$X$($n$)) = expectation($p$;$f$($m$);$X$($m$)) $\in$ $\mathbb{Q}$ \\[0ex]\& expectation($p$;$f$($n$);($x$.$x$ $\ast$ $x$) o $X$($n$)) = expectation($p$;$f$($m$);($x$.$x$ $\ast$ $x$) o $X$($m$)) $\in$ $\mathbb{Q}$ \\[0ex]\& \=expectation($p$;$f$($n$);($x$.($x$ $\ast$ $x$) $\ast$ $x$) o $X$($n$))\+ \\[0ex]= \\[0ex]expectation($p$;$f$($m$);($x$.($x$ $\ast$ $x$) $\ast$ $x$) o $X$($m$)) \\[0ex]$\in$ $\mathbb{Q}$ \-\\[0ex]\& \=expectation($p$;$f$($n$);($x$.($x$ $\ast$ $x$) $\ast$ $x$ $\ast$ $x$) o $X$($n$))\+ \\[0ex]= \\[0ex]expectation($p$;$f$($m$);($x$.($x$ $\ast$ $x$) $\ast$ $x$ $\ast$ $x$) o $X$($m$)) \\[0ex]$\in$ $\mathbb{Q}$ \-\- \end{tabbing}